/*********************************************************************
Author: Roberto Bruttomesso <roberto.bruttomesso@unisi.ch>

MiniWrapper -- Copyright (C) 2008, Roberto Bruttomesso

MiniWrapper is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

MiniWrapper is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with MiniWrapper. If not, see <http://www.gnu.org/licenses/>.
*********************************************************************/

#include "Solver.h"
#include <map>
#include <string>
#include <cstring>
#include <iostream>

#include <sys/time.h>
#include <sys/resource.h>
#include <unistd.h>

using namespace std;

static inline double cpuTime(void) {
    struct rusage ru;
    getrusage(RUSAGE_SELF, &ru);
    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }

extern int yyparse( void * );
extern int yyrestart( FILE * );

Solver S;
map< string, Var > string_to_var;

struct parser_data
{
  Solver S;
  map< string, Var > string_to_var;
  map< Var, string > var_to_string;
};

int main( int argc, char * argv[] )
{
  FILE * in;

  if ( argc != 2 && argc != 3 )
  {
    cerr << "Usage: " << argv[0] << " [-m] filename" << endl;
    exit( 1 );
  }

  if ( argc == 3 && strcmp(argv[1],"-m") != 0 )
  {
    cerr << "Usage: " << argv[0] << " [-m] filename" << endl;
    exit( 1 );
  }

  if ( (in = fopen( argv[argc-1], "rt" )) == NULL )
  {
    cerr << "Can't open file " << argv[1] << endl;
    exit( 1 );
  }

  struct parser_data data;

  cout << "Parsing ... ";
  fflush(stdout);

  yyrestart( in );
  yyparse( (void *) &data );

  cout << "done ( time elapsed " << cpuTime() << " s )" << endl;
  cout << "Solving ... ";
  fflush(stdout);

  lbool result = data.S.solve( );

  cout << "done ( time elapsed " << cpuTime() << " s )" << endl;
  fflush(stdout);

  if ( result == l_Undef )
  {
    cerr << "Something wrong happend" << endl;
    exit( 1 );
  }

  cout << "The problem is: ";

  if ( result == l_False )
    cout << "unsatisfiable" << endl;
  else if ( result == l_True )
  {
    cout << "satisfiable" << endl;
    if ( argc == 3 )
      data.S.printModel( data.var_to_string );
  }

  return 0;
}
